$\forall$$A$:Type, $B$:($A$$\rightarrow$Type). fpf{-}empty $\in$ fpf($A$; $x$.$B$($x$))